

\documentclass[usenames,dvipsnames,svgnames,x11names,pdftex]{beamer}

%\usetheme{Darmstadt}
%\usetheme{AnnArbor}
%\usetheme{Frankfurt}
%\usetheme{Ilmenau}
\usetheme{Copenhagen}
\usefonttheme[onlylarge]{structurebold}
\setbeamerfont*{frametitle}{size=\normalsize,series=\bfseries}
\setbeamertemplate{navigation symbols}{}

\usepackage{k2latex.bb}

\usepackage[english]{babel}
\usepackage[latin1]{inputenc}
\usepackage{times}
\usepackage[T1]{fontenc}
\usepackage{pifont}

% Setup TikZ

\usepackage{tikz}
\usetikzlibrary{arrows}
\tikzstyle{block}=[draw opacity=0.7,line width=1.4cm]

\newcommand{\tick}{\ding{52}}

\pagenumbering{arabic}

\begin{document}


% Author, Title, etc.

\title{Contextual transformation in K Framework}
\author{Andrei Arusoaie}
\institute{Faculty of Computer Science, UAIC, Ia\c{s}i}
\date{July 2, 2011}  



% The main document

\begin{frame}
  \titlepage
  \begin{center}\textnormal{Advisor: Prof. PhD. DOREL Lucanu}\end{center}
\end{frame}

\begin{frame}{Outline}
  \tableofcontents
\end{frame}


\section{\K}

\subsection{\K Framework - short overview}


%\begin{frame}{\K Project}
%Started in 2003 by Grigore Ro{\c s}u at UIUC, motivated mainly by teaching programming languages and noticing that the existing semantic frameworks have limitations
%\bigskip
%
%A rewriting-based framework optimized for defining programming languages
%
%\end{frame}
%
%\begin{frame}{\K{}ontributors}
%Joint work between Formal Systems Laboratory (FSL) from University of Illinois at Urbana-Champaign (UIUC) lead by Grigore Ro\c{s}u and Formal Methods in Software Engineering (FMSE) from Al. I. Cuza University (UAIC) lead by Dorel Lucanu
%\medskip
%
%UIUC team:\\
%Chucky Ellison, Patrick Meredith, Grigore Ro\c{s}u, Traian Florin \c{S}erb\u{a}nu\c{t}\u{a}, Andrei \c{S}tef\u{a}nescu, David Laz{\u a}r
%\medskip
%
%UAIC team:\\
%Irina M{\u a}riuca As{\u a}voae, Mihai As{\u a}voae, Gheorghe Grigora{\c s}, Dorel Lucanu, Radu Mereu{\c t}{\u a}, Elena Naum  
%
%\end{frame}



\begin{frame}{\K Ingredients}
\begin{itemize}
\item \structure{Computations} 
\begin{itemize} 
\item Sequences of tasks, including syntax 
\item Capture the sequential fragment of programming languages 
\item Syntax annotations specify order of evaluation
\end{itemize}
\item \alert{Configurations} 
\begin{itemize}
\item Multisets (bags) of nested cells 
\item High potential for concurrency and modularity
\end{itemize}
\item \alert{\K rules} 
\begin{itemize}
\item Specify only what needed, precisely identify what changes 
\item More concise, modular, and concurrent than regular rewrite rule
\end{itemize}
\end{itemize}
\end{frame}




\subsection{SIMPLE language}


\begin{frame}[t]{SIMPLE}
  \begin{block}{SIMPLE language}
    \begin{itemize}
    \item Imperative programming paradigm and some additional features
    \end{itemize}
  \end{block}

Additional features:
%  \begin{block}{Additional features}
    \begin{itemize}
    \item Multidimensional arrays and arrays references
    \item Functions and functions references
    \item Blocks with locals
    \item Input/Output
    \item Exceptions
    \item Concurrency (thread creation/termination, syncronization)
    \end{itemize}
%  \end{block}
\end{frame}



\begin{frame}[t]{SIMPLE - configuration}

\centering
\includegraphics[scale=0.6]{configuration.pdf}  

\end{frame}



\subsection{Variable lookup}


\begin{frame}[t]{Variable lookup rule}

\begin{example}[Variable lookup]
When 
\begin{itemize}
\item X is the first computational task, and
\item X is bound to some location L, and
\item L is mapped to some value V
\end{itemize}
 then rewrite X by L
\end{example}

\centering
\includegraphics[scale=0.7]{rule1.pdf}  

\end{frame}



\begin{frame}{Simple: sample configuration}{\only<1>{heating ...}\only<2>{apply variable lookup rule ...}\only<3,4>{cooling ...}\only<5>{and so on ...}}
%\hspace{5ex}
%\begin{block}{Rule}
\centering
\includegraphics[scale=0.7]{rule1.pdf}  
%\end{block}


%\begin{minipage}{\textwidth}
\fontsize{7}{7}\selectfont
%\hspace{-1.5cm}
\kallLarge{red}{T}{\kallLarge{orange}{threads}{\kallLarge{yellow}{thread *}{\kallLarge{green}{\alert<2>{k}}{\only<1,2,3,4>{\alert<2->{\only<1,2>{x}\only<3,4>{10}} \kra} a = \only<1,2,3,4>{\square}\only<5>{\alert<5>{10}} \kra a = x \mathrel{} ... }\mathrel{}\kallLarge{violet}{\alert<2,3>{env}}{a \mapsto 1 \mathrel{} \alert<2,3>{x \mapsto 5} }}}\kBR \mathrel{}\kallLarge{white}{\alert<2,3>{store}}{ ... \mathrel{} \alert<2,3>{5 \mapsto 10} \mathrel{} ... }}
%\end{minipage}\\
\end{frame}









\section{Contextual Transformation}

\subsection{Contextual Transformation}

\begin{frame}[t]{Contextual Transformation}

\begin{block}{Rewrite rules}
\begin{itemize}
\item \K is a rewriting-based framework ...
\item Rewriting rules: A $\Rightarrow$ B
\item If the lhs (A) {\it matches} a term T, then the rule can be applied: rewrite A by B
\end{itemize}
\end{block}

\begin{block}{\alert{Problem!}}
\begin{itemize}
\item \K rules are not always term rewrite rules!
\item Solution: transform a \K rule according to a given configuration into a rewrite rule.
\end{itemize}
\end{block}

\end{frame}


\begin{frame}[t]{Context transformation}

\begin{block}{Solution}
Variable lookup rule - full context
\end{block}
\centering
\includegraphics[scale=0.7]{rule2.pdf}  
  

\end{frame}


\begin{frame}[t]{Contextual Transformation}
\begin{block}{Shortcomings of the existing implementation}

\begin{enumerate}
\item Cells with the same label are not allowed
\item The cases when the context transformation could have more than one solution are not analyzed
\item There are cases in which the current algorithm could have undefined behaviors
\item The \structure{Locality Principle} does not have yet an unanimously agreed formal specification
\item Only the minimal unambiguous context is computed
\end{enumerate}
\end{block}

\end{frame}

\subsection{Approach}

\begin{frame}[t]{Contextual Transformation}
\vspace{1cm}
\begin{block}{Our approach}
\begin{enumerate}
\item Find \alert{all} \structure{witnesses} (mappings between rule and configuration cells)
\item Generate \alert{all} possible \structure{variants} for each witness
\item Apply \structure{Locality Principle} (formal definition)
\item \structure{Consistency} checking
\item \structure{Disambiguation}
\end{enumerate}
\end{block}

\end{frame}

\subsection{Example}

\begin{frame}[t]{Contextual Transformation}

\fontsize{7}{7}\selectfont

\begin{example}[Configuration]
\centering
\begin{minipage}{.6\textwidth}
\kallLarge{white}{T}{\kallLarge{white}{server}{\kallLarge{red}{k *}{\dotCt{K}}}\mathrel{}\kallLarge{white}{client *}{\kallLarge{blue}{k}{\dotCt{K}}}}
\end{minipage}\\
\end{example}

\begin{example}[Synchronous comunication]
\centering
{\ensuremath{{\kall{magenta}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{magenta}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}}
\end{example}
 
\end{frame}



\begin{frame}[t]{1. W = getAllWitnesses(C, R)}

\begin{tabular}{l r}
\fontsize{5}{7}\selectfont

\begin{minipage}{.6\textwidth}
\kallLarge{white}{T}{\kallLarge{white}{server}{\kallLarge{red}{k *}{\dotCt{K}}}\mathrel{}\kallLarge{white}{client *}{\kallLarge{blue}{k}{\dotCt{K}}}}
\end{minipage}
&
\fontsize{9}{9}\selectfont
\hspace{7ex}
\begin{tabular}{l@{}l}
W = \{
& \only<1->{({\color{red!50!black}$k_{server}$}; {\color{red!50!black}$k_{server}$}),} \\
& \only<2->{({\color{red!50!black}$k_{server}$}; {\color{blue!50!black}$k_{client}$}),} \\
& \only<3->{({\color{blue!50!black}$k_{client}$}; {\color{red!50!black}$k_{server}$}),} \\
& \only<4>{({\color{blue!50!black}$k_{client}$}; {\color{blue!50!black}$k_{client}$})\}} \\
\end{tabular}
\end{tabular}
\vspace{2ex}

\fontsize{7}{7}\selectfont

\begin{tabular*}{\textwidth}{l r}
\only<1->{\ensuremath{{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{red}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}} &

\hspace{10ex}\only<2->{\ensuremath{{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}} \vspace{5ex} \\

\only<3->{\ensuremath{{\kall{blue}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{red}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}} &

\hspace{10ex}\only<4>{\ensuremath{{\kall{blue}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}}

\end{tabular*}

\end{frame}



\begin{frame}[t]{1. T = getAllVariants(W)}
\fontsize{7}{7}\selectfont

% first row - tree: red red
\begin{tabular*}{\textwidth}{l c@{} r}
\only<1->{{\ensuremath{{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{red}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}} &  $\rightarrow$ &

{\ensuremath {\kall{white}{T}{\kall{white}{server}{{{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{red}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}}}}}} \\



% second row - tree: red green
\only<2>{{\ensuremath{{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}} 
&$\rightarrow$ &
{\ensuremath{ \kall{white}{T}{{\hspace{-4ex}{\kall{white}{server}{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}}\mathrel{\terminal{}}{\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}\hspace{-4ex}}}}}} \\

\end{tabular*}
\end{frame}




\begin{frame}[t]{2. T = getAllVariants(W)}
\fontsize{7}{7}\selectfont

\begin{tabular*}{\textwidth}{l c@{} r}
% third row - tree: green red
\only<1->{\ensuremath{{\kall{blue}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{red}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}}
& $\rightarrow$ &
{\ensuremath{ \kall{white}{T}{{\hspace{-4ex}{\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}}\mathrel{\terminal{}}{\kall{white}{server}{\kall{red}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}\hspace{-4ex}}}}} \\

\only<2>{{\ensuremath{{\kall{blue}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}}
& $\rightarrow$ & 
${\ensuremath \kall{white}{T}{{\hspace{-4ex}{\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}}\mathrel{\terminal{}}{\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}\hspace{-4ex}}}}$}

\end{tabular*}

\end{frame}



\begin{frame}[t]{3. Apply Locality Principle on T: $T_1\preccurlyeq T_2$ if $|V_{T_1}| \leq |V_{T_2}|$}

\fontsize{5}{5}\selectfont

\begin{tabular*}{\textwidth}{l r}


\begin{minipage}{.5\textwidth}
{\ensuremath {\kall{white}{T}{\kall{white}{server}{{{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\mathrel{\terminal{}}{\kall{red}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}}}}}\\
\fontsize{9}{9}\selectfont
\vspace{3ex}
\centering \only<2>{No of cells: 4}\only<3>{\color{green}{No of cells: 4}\tick}
%\vspace{3ex}
\end{minipage}&


\begin{minipage}{.5\textwidth}
\hspace{-3ex}{\ensuremath{ \kall{white}{T}{{\hspace{-4ex}{\kall{white}{server}{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}}\mathrel{\terminal{}}{\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}\hspace{-4ex}}}}} \\
\fontsize{9}{9}\selectfont
\vspace{3ex}
\centering \only<2>{No of cells: 5}\only<3>{\color{red}{No of cells: 5}}
\end{minipage}\\


\begin{minipage}{.5\textwidth}
\hspace{-4ex}{\ensuremath{ \kall{white}{T}{{\hspace{-4ex}{\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}}\mathrel{\terminal{}}{\kall{white}{server}{\kall{red}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}\hspace{-4ex}}}}}\\
\fontsize{9}{9}\selectfont
\vspace{3ex}
\centering \only<2>{No of cells: 5}\only<3>{\color{red}{No of cells: 5}}
\end{minipage}&


\begin{minipage}{.5\textwidth}
\hspace{-3ex}${\ensuremath \kall{white}{T}{{\hspace{-4ex}{\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}}\mathrel{\terminal{}}{\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}}\hspace{-4ex}}}}$\\
\fontsize{9}{9}\selectfont
\vspace{3ex}
\centering \only<2>{No of cells: 5}\only<3>{\color{red}{No of cells: 5}}
\end{minipage}

\end{tabular*}

\end{frame}





\begin{frame}[t]{4. Disambiguation}
\centering

\only<1->{\begin{minipage}{\textwidth}
\fontsize{7}{7}\selectfont
\kallLarge{white}{T}{\kallLarge{white}{server}{\kallLarge{red}{k}{\dotCt{K}}}\mathrel{}\kallLarge{white}{client *}{\kallLarge{blue}{k}{\dotCt{K}}}\mathrel{}\kallLarge{white}{agent *}{\kallLarge{white}{a}{\dotCt{Map}}\mathrel{}\kallLarge{green}{k}{\dotCt{K}}\mathrel{}\kallLarge{white}{b}{\dotCt{Set}}}}
\vspace{5ex}
\end{minipage}}

\begin{tabular*}{\textwidth}{c c}
\only<2,3>{\begin{minipage}{.5\textwidth}
\fontsize{5}{5}\selectfont
${\ensuremath \kall{white}{T}{{{\hspace{-3ex}\kall{white}{server}{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\hspace{-3ex}}\mathrel{\terminal{}}{\hspace{-3ex}\kall{white}{client}{\kall{blue}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}}\hspace{-3ex}}}}}$
\end{minipage}}
 &
\only<2>{\begin{minipage}{.5\textwidth}
\fontsize{5}{5}\selectfont
${\ensuremath \kall{white}{T}{{{\hspace{-3ex}\kall{white}{server}{\kall{red}{k}{\reduce{{\terminal{send}{\variable{V}{KResult}}\terminal{on}{\variable{C}{Id}}}}{\dotCt{K}}}}\hspace{-3ex}}\mathrel{\terminal{}}{\kmiddle{white}{agent}{\hspace{-1ex}\kall{green}{k}{\reduce{{\terminal{receive on}{\variable{C}{Id}}}}{\variable{V}{KResult}}}\hspace{-1ex}}}}}}$\\
\end{minipage}}
\only<3>{\Huge{\color{green}\tick}}
\end{tabular*}

\end{frame}

\section{Conclusions}

\begin{frame}[t]{Conclusions}

\begin{block}{Contributions}
\begin{enumerate}
\item Contextual transformation - complete description
\item Formal definitions: \structure{witness}, \structure{locality principle}
\item Several algorithms: finding all witnesses, variants, apply locality principle
\end{enumerate}
\end{block}

\begin{block}{Future work}
\begin{enumerate}
\item Cell creation/deletion + disambiguation
\item Complete open cells
\item Anonymous variables
\item Translation to Maude
\end{enumerate}
\end{block}


\end{frame}

\end{document}






%\begin{frame}[t]{1. W = getAllWitnesses(C, R)}
%
%%\begin{tabular}
%
%%\end{tabular}
%%\fontsize{7}{7}\selectfont
%\begin{minipage}{\textwidth}
%\hspace{-10ex}\kallLarge{white}{top}
%{
%\kallLarge{white}{feasable}{}\hspace{-3ex}
%\kallLarge{white}{infeasable}{}\hspace{-3ex}
%\kallLarge{white}{check}{}\hspace{-3ex}
%\kallLarge{white}{mainOut}{}\hspace{-3ex}\kBR
%\hspace{-7.5ex}\kallLarge{white}{tasks}
%    {
%    \hspace{-4ex}\kallLarge{white}{funTask*}
%        {
%        \kallLarge{white}{funId}{}
%        \kallLarge{white}{task*}{}
%        \kallLarge{white}{taskType}{}\kBR
%        \kallLarge{white}{configuration}{}
%        \kallLarge{white}{form}{}
%        \kallLarge{white}{subst}{}
%        }\hspace{-4ex}
%    }\hspace{-7.5ex}
%}
%\end{minipage}
%\end{frame}
%
%
%\begin{frame}
%\kallLarge{white}{config}
%{
%    \kallLarge{white}{program}{}
%    \kallLarge{white}{struct}{}
%    \kallLarge{white}{fun}{}
%    \kallLarge{white}{k}{}\kBR
%    \kallLarge{white}{env}{}
%    \kallLarge{white}{stack}{}
%    \kallLarge{white}{fname}{}
%    \kallLarge{white}{tenv}{}\kBR
%    \kallLarge{white}{heap}{}
%    \kallLarge{white}{in}{}
%    \kallLarge{white}{out}{}
%    \kallLarge{white}{couner}{}
%}
%\end{frame}
